@book{peano1889,
  title={Arithmetices principia: nova methodo},
  author={Peano, G.},
  year={1889},
  publisher={Fratres Bocca}
}
@article{Rehof1996,
 author = {Rehof, J.},
 title = {Strong normalization for non-structural subtyping via saturated sets},
 journal = {Inf. Process. Lett.},
 volume = {58},
 issue = {4},
 month = {May},
 year = {1996},
 issn = {0020-0190},
 pages = {157--162},
 numpages = {6},
 url = {http://dx.doi.org/10.1016/0020-0190(96)00056-7},
 doi = {http://dx.doi.org/10.1016/0020-0190(96)00056-7},
 acmid = {231179},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Lambda calculus, functional programming, programming calculi, programming languages, strong normalization, subtyping},
}
@article{Takahashi95,
  author    = {M. Takahashi},
  title     = {Parallel Reductions in lambda-Calculus},
  journal   = {Inf. Comput.},
  volume    = {118},
  number    = {1},
  year      = {1995},
  pages     = {120-127},
  ee        = {http://dx.doi.org/10.1006/inco.1995.1057},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{hindley1969principal,
  title={The principal type-scheme of an object in combinatory logic},
  author={Hindley, R.},
  journal={Transactions of the american mathematical society},
  pages={29--60},
  year={1969},
  publisher={JSTOR}
}
@ARTICLE{Mogensen94,
    author = { Mogensen, T.},
    title = {Efficient Self-Interpretation in Lambda Calculus},
    journal = {Journal of Functional Programming},
    year = {1994},
    volume = {2},
    pages = {345--364}
}
@article{milner1978theory,
  title={A theory of type polymorphism in programming},
  author={Milner, R.},
  journal={Journal of computer and system sciences},
  volume={17},
  number={3},
  pages={348--375},
  year={1978},
  publisher={Elsevier}
}
@inproceedings{Coppo:1978,
 author = {Coppo, M. and Dezani-Ciancaglini, M. and Rocca, S. R. D.},
 title = {(Semi)-separability of Finite Sets of Terms in Scott's $\mathrm{D}_{\infty}$-Models of the lambda-Calculus},
 booktitle = {Proceedings of the Fifth Colloquium on Automata, Languages and Programming},
 year = {1978},
 isbn = {3-540-08860-1},
 pages = {142--164},
 numpages = {23},
 url = {http://dl.acm.org/citation.cfm?id=646232.682078},
 acmid = {682078},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 

@book{whitehead1927principia,
  title={Principia mathematica. 2.1927},
  author={Whitehead, A.N. and Russell, B.},
  lccn={lc25015133},
  series={Principia Mathematica},
  url={http://books.google.com/books?id=JCMgAQAAIAAJ},
  year={1927},
  publisher={Cambridge University Press}
}
@book{Barendregt:1985,
  title={The lambda calculus: Its syntax and semantics},
  author={Barendregt, H.},
  volume={103},
  year={1985},
  publisher={North Holland}
}
@article{zermelo1908untersuchungen,
  title={Untersuchungen {\"u}ber die Grundlagen der Mengenlehre. I},
  author={Zermelo, E.},
  journal={Mathematische Annalen},
  volume={65},
  number={2},
  pages={261--281},
  year={1908},
  publisher={Springer}
}

@article{quine1937new,
  title={New foundations for mathematical logic},
  author={Quine, W. V.},
  journal={The American mathematical monthly},
  volume={44},
  number={2},
  pages={70--80},
  year={1937},
  publisher={JSTOR}
}
@dissertation{Girard:72,
author="J.-Y. Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}

@book{Girard:1989,
 author = {Girard, J.-Y. and Taylor, P. and Lafont, Y.},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 
@incollection{Bove:2009,
  title={A brief overview of Agda--a functional language with dependent types},
  author={Bove, A. and Dybjer, P. and Norell, U.},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={73--78},
  year={2009},
  publisher={Springer}
}

@article{Coq,
  title={The Coq Proof Assistant Reference Manual},
  author={The Coq Development Team},
  journal={Version 8.3. INRIA},
  publisher={Available from http://coq.inria.fr/V8.3/refman/},
  year={2010}
}

@book{takeuti1975proof,
  title={Proof Theory},
  author={Takeuti, G.},
  lccn={75023164},
  series={Volume 81 of Studies in logic and the foundations of mathematics, ISSN 0049-237X},
  url={http://books.google.com/books?id=tMSEAAAAIAAJ},
  year={1975},
  publisher={North-Holland Publishing Company}
}


@article{leroy1998ocaml,
  title={The OCaml programming language},
  author={Leroy, X.},
  journal={Online},
  url={http://caml. inria. fr/ocaml/index.en.html},
  year={1998}
}

@book{jones2003haskell,
  title={Haskell 98 language and libraries: the revised report},
  author={Peyton Jones, S. L.},
  year={2003},
  publisher={Cambridge University Press}
}
@book{peyton1987,
  title={The implementation of functional programming languages (prentice-hall international series in computer science)},
  author={Peyton Jones, S. L.},
  year={1987},
  publisher={Prentice-Hall, Inc.}
}
@inproceedings{jones1999,
  title={Typing haskell in haskell},
  author={Jones, M. P.},
  booktitle={Haskell workshop},
  volume={43},
  pages={45},
  year={1999}
}
@article{church1940,
  title={A formulation of the simple theory of types},
  author={Church, A.},
  journal={The journal of symbolic logic},
  volume={5},
  number={2},
  pages={56--68},
  year={1940},
  publisher={JSTOR}
}

@book{Church:1985,
 author = {Church, A.},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
 isbn = {0691083940},
 publisher = {Princeton University Press},
 address = {Princeton, NJ, USA},
}

@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}

@phdthesis{vaninwegen1996machine,
  title={The machine-assisted proof of programming language properties},
  author={VanInwegen, M.},
  year={1996},
  school={University of Pennsylvania}
}

@inproceedings{parigot1988programming,
  title={Programming with proofs: a second order type theory},
  author={Parigot, M.},
  booktitle={ESOP'88},
  pages={145--159},
  year={1988},
  organization={Springer}
}

@book{Winskel:1993,
 author = {Winskel, G.},
 title = {The formal semantics of programming languages: an introduction},
 year = {1993},
 isbn = {0-262-23169-7},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
} 
@phdthesis{Raffalli:1994,
  title={L' Arithm\'etiques Fonctionnelle du Second Ordre avec Points Fixes},
  author={C. RAFFALLI},
  year={1994},
  school={L'universit\'e Paris VII}
}

@book{matthes1999extensions,
  title={Extensions of system F by iteration and primitive recursion on monotone inductive types},
  author={Matthes, R.},
  year={1999},
  publisher={Herbert Utz Verlag}
}

@inproceedings{fu2011framework,
  title={A Framework for Internalizing Relations into Type Theory},
  author={Fu, P. and Stump, A. and Vaughan, J.},
  booktitle={PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories},
  year={2011}
}

@article{krivine2002lambda,
  title={Lambda-calculus types and models},
  author={Krivine, J.-L.},
  year={2002}
}

@misc{frege1967basic,
  title={The Basic Laws of Arithmetic: Exposition of the System, translated and edited with an introduction by Montgomery Furth},
  author={Frege, G.},
  year={1967},
  publisher={University of California Press}
}
@book{hatcher:1982,
  title={The logical foundations of mathematics},
  author={Hatcher, W. S.},
  volume={10},
  year={1982},
  publisher={Pergamon Press Oxford}
}

@inproceedings{leivant1983reasoning,
  title={Reasoning about functional programs and complexity classes associated with type disciplines},
  author={Leivant, D.},
  booktitle={Foundations of Computer Science, 1983., 24th Annual Symposium on},
  pages={460--469},
  year={1983},
  organization={IEEE}
}

@INPROCEEDINGS{Barendregt:92,
    author = {H. Barendregt},
    title = {Lambda Calculi with Types},
    booktitle = {Handbook of Logic in Computer Science},
    year = {1992},
    pages = {117--309},
    publisher = {Oxford University Press}
}

%% paper
@manuscript{Abadi:93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  

@techreport{mendler:1987,
  title={Inductive definition in type theory},
  author={P. Mendler},
  year={1987},
  institution={Cornell University}
}
@techreport{coquand:inria-00075471,
    hal_id = {inria-00075471},
    url = {http://hal.inria.fr/inria-00075471},
    title = {{Metamathematical investigations of a calculus of constructions}},
    author = {T. Coquand},
    language = {English},
    affiliation = {INRIA Rocquencourt - INRIA Rocquencourt},
    institution = {INRIA},
    number = {RR-1088},
    year = {1989},
    month = Sep,
    pdf = {http://hal.inria.fr/inria-00075471/PDF/RR-1088.pdf},
}
 

@article{Barendregt:97,
  author    = {H. Barendregt},
  title     = {The impact of the lambda calculus in logic and computer
               science},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {3},
  number    = {2},
  year      = {1997},
  pages     = {181-215},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0302/0302-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Werner:92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
pages="341--357",
}
@book{Pierce2002,
                   author = {Pierce, Benjamin C.},
                   title = {Types and programming languages},
                   year = {2002},
                   isbn = {0-262-16209-1},
                   publisher = {MIT Press},
                   address = {Cambridge, MA, USA},
                   }

@article{Coquand:1988,
 author = {T. Coquand and G. Huet},
 title = {The calculus of constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 pages = {95--120},
} 
@incollection{Paulin:1993,
  title={Inductive definitions in the system coq rules and properties},
  author={C. Paulin-Mohring},
  booktitle={Typed lambda calculi and applications},
  pages={328--345},
  year={1993},
}
@article{Jansen:2011,
  author    = {J.M. Jansen and R. Plasmeijer and P. Koopman},
  title     = {Functional Pearl: Comprehensive Encoding of Data Types and Algorithms in the lambda-Calculus},
  journal   = {Internal report, NLDA},
  year      = {2011},
}
@phdthesis{miquel:2001,
  title={Le Calcul des Constructions implicite: syntaxe et s{\'e}mantique},
  author={A. Miquel},
  year={2001},
  school={PhD thesis, Universit{\'e} Paris 7}
}
@incollection{ahn:2013,
  title={System {Fi}},
  author={K.Y. Ahn and T. Sheard and M. Fiore and A.M. Pitts},
  booktitle={Typed Lambda Calculi and Applications},
  pages={15--30},
  year={2013},
}

@article{Hardin:1989,
 author = {T. Hardin},
 title = {Confluence results for the pure strong categorical logic CCL. $\lambda$-calculi as subsystems of CCL},
 journal = {Theoretical Computer Science},
 volume = {65},
 number = {3},
 month = jul,
 year = {1989},
 pages = {291--342},
} 
@article{Rosen:1973,
 author = {B. Rosen},
 title = {Tree-Manipulating Systems and Church-Rosser Theorems},
 journal = {J. ACM},
 volume = {20},
 number = {1},
 year = {1973},
 pages = {160--187},
} 
@phdthesis{hindley1964,
  title={The Church-Rosser property and a result in combinatory logic.},
  author={J. Hindley},
  year={1964},
  school={University of Newcastle upon Tyne}
}

@inproceedings{kuan2007,
  title={A rewriting semantics for type inference},
  author={G. Kuan and D. MacQueen and R. Findler},
  booktitle={Proceedings of the 16th European Symposium on Programming},
  pages={426--440},
  year={2007},
}

@inproceedings{stump2011,
  title={Type Preservation as a Confluence Problem.},
  author={A. Stump and G. Kimmell and R. Omar},
  booktitle={Rewriting Techniques and Applications},
  pages={345--360},
  year={2011}
}

@manuscript{fu+14,
author={P. Fu and A. Stump},
title={{Self Types for Dependently Typed Lambda Encodings}},
note="Extended version available from \url{http://homepage.cs.uiowa.edu/~pfu/document/papers/rta-tlca.pdf}",
year=2014}

@misc{barendregt:1993,
  title={Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures},
  author={H. Barendregt},
  year={1993},
}

@article{Ariola:1997,
title = "Lambda Calculus with Explicit Recursion ",
journal = "Information and Computation ",
volume = "139",
number = "2",
pages = "154 -- 233",
year = "1997",
author = "Z. Ariola and J. Klop"
}


@article{barras10,
	author = {B. Barras},
	title = {Sets in Coq, Coq in Sets},
	journal = {Journal of Formalized Reasoning},
	volume = {3},
	number = {1},
	year = {2010}
}

@phdthesis{werner:phd,
  author = "B. Werner",
  title = "Une th\'{e}orie des constructions inductives",
  school = "Universit\'{e} Paris VII",
  year = 1994,
}

@PHDTHESIS{gimenez96,
url = "http://www.theses.fr/1996ENSL0044",
title = "Un calcul de constructions infinies et son application a la verification de systemes communicants",
author = "E. Gimenez",
year = "1996",
}


@inproceedings{abel+13,
  author    = {A. Abel and
               B. Pientka},
  title     = {Wellfounded recursion with copatterns: a unified approach
               to termination and productivity},
  year      = {2013},
  pages     = {185--196},
  editor    = {G. Morrisett and
               T. Uustalu},
  booktitle     = {International Conference on Functional Programming (ICFP)},
}

@article{capretta05,
  author    = {V. Capretta},
  title     = {General recursion via coinductive types},
  journal   = {Logical Methods in Computer Science},
  volume    = {1},
  number    = {2},
  year      = {2005},
}

@misc{schepler13,
author = {D. Schepler},
title = "bijective function implies equal types is provably inconsistent with functional extensionality in Coq",
note = "message to the Coq Club mailing list, December 12, 2013"}

@inproceedings{geuvers94,                  
title = {{Inductive and Coinductive Types with Iteration and Recursion}},
author = "H. Geuvers",
year = 1994,
booktitle="Informal proceedings of the 1992 workshop on Types for Proofs and Programs",
editor="B. Nordstrom and K. Petersson and G. Plotkin",
pages="183--207"}.

@inproceedings{geuvers01,
  author    = {H. Geuvers},
  title     = {{Induction Is Not Derivable in Second Order Dependent Type
               Theory}},
  booktitle = {Typed Lambda Calculi and Applications (TLCA)},
  year      = {2001},
  pages     = {166-181},
}

@inproceedings{parigot88,
  author    = {M. Parigot},
  title     = {{Programming with Proofs: A Second Order Type Theory}},
  year      = {1988},
  pages     = {145-159},
  editor    = {H. Ganzinger},
  booktitle     = {Proceedings of the 2nd European Symposium on Programming (ESOP)},
}
@book{martin:1984,
  title={Intuitionistic type theory},
  author={Martin-L\"of, P. and Sambin, G.},
  volume={17},
  year={1984},
  publisher={Bibliopolis Naples,, Italy}
}
@inproceedings{casinghino2014,
  title={Combining proofs and programs in a dependently typed language},
  author={Casinghino, C. and Sj{\"o}berg, V. and Weirich, S.},
  booktitle={Proceedings of the 41st annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={33--46},
  year={2014},
  organization={ACM}
}
@inproceedings{kimmell2012,
  title={Equational reasoning about programs with general recursion and call-by-value semantics},
  author={Kimmell, G. and Stump, A. and Eades III, H. D. and Fu, P. and Sheard, T. and Weirich, S. and Casinghino, C. and Sj{\"o}berg, V. and Collins, N. and Ahn, K. Y.},
  booktitle={Proceedings of the sixth workshop on Programming languages meets program verification},
  pages={15--26},
  year={2012},
  organization={ACM}
}                  
@inproceedings{altenkirch+10,
  author    = {T. Altenkirch and
               N. Danielsson and
               A. L{\"o}h and
               N. Oury},
  title     = {PiSigma: Dependent Types without the Sugar},
  year      = {2010},
  pages     = {40-55},
  editor    = {M. Blume and
               N. Kobayashi and
               G. Vidal},
  booktitle     = {10th International Symposium on Functional and Logic Programming (FLOPS)},
}

@INPROCEEDINGS{hickey96,
    author = {J. Hickey},
    title = {Formal Objects in Type Theory Using Very Dependent Types},
    editor={K. Bruce} ,                 
    booktitle = {In Foundations of Object Oriented Languages (FOOL) 3},
    year = {1996}
}

@inproceedings{odersky+03,
  author    = {M. Odersky and
               V. Cremet and
               C. R{\"o}ckl and
               M. Zenger},
  title     = {{A Nominal Theory of Objects with Dependent Types}},
  booktitle = {17th European Conference on Object-Oriented Programming
                  (ECOOP)},
  year      = {2003},
  pages     = {201-224},
  editor    = {L. Cardelli},
}

@TECHREPORT{crary99,
    author = {K. Crary},
    title = {{Simple, Efficient Object Encoding using Intersection Types}},
    institution = {Carnegie Mellon University},
    number={CMU-CS-99-100},
    year = {1999}
}

@INPROCEEDINGS{abadi+94,
    author = {M. Abadi and L. Cardelli},
    title = {{A Theory of Primitive Objects - Second-Order Systems}},
    booktitle = {European Symposium on Programming (ESOP)},
    year = {1994},
    pages = {1--25},
}

@phdthesis{vau09,
  author = {J. A. Vaughan},
  title  = {Aura: Programming with Authorization and Audit},
  school = {University of Pennsylvania},
  year   = {2009},
  address = {Philadelphia}
}

@book{nordstrom90:programming-tt,
    address = {USA},
    author = {Nordstr\"{o}m, B. and Petersson, K. and Smith, J. M.},
    isbn = {0198538146},
    month = {July},
    publisher = {Oxford University Press},
    title = {{Programming in Martin-L\"{o}f's Type Theory: An Introduction}},
    url = {http://www.cs.chalmers.se/Cs/Research/Logic/book/},
    year = {1990}
}
@inproceedings{sjoberg+10,
author={V. Sj{\"o}berg and A. Stump},
title={{Equality, Quasi-Implicit Products, and Large Eliminations}},
booktitle="Workshop on Intersection Types and Related Systems (ITRS)",
editor="B. Venneri",                  
year=2010}
